Nuprl Definition : equiv_rel 13,42
compound
EquivRel(T;x,y.E(x;y)) == Refl(T;x,y.E(x;y)) & Sym(T;x,y.E(x;y)) & Trans(T;x,y.E(x;y)) 
latex

Uprel 1, rel 1
Wellformedness Lemmasequiv rel wf, equiv rel wf
DefinitionsRefl(T;x,y.E(x;y)), P & Q, Sym(T;x,y.E(x;y)), Trans(T;x,y.E(x;y))
FDL editor aliasesequiv_rel

origin